Nuprl Lemma : EState_wf
11,40
postcript
pdf
T
:(Id
Type). EState(
T
)
Type
latex
Definitions
EState(
T
)
,
x
:
A
.
B
(
x
)
,
rationals
,
f
(
a
)
,
x
:
A
B
(
x
)
,
Id
,
t
T
,
Type
Lemmas
Id
wf
,
rationals
wf
origin
T:(Id
Type). EState(T) 
Type T:(IdType). EState(T) Type x:A. B(x)B(x) T